Old Exams

For the first part, we consider the solution terminated if all its constituent processes have terminated.

The rest of the question is an odd fit: \(P\) is an open system, so most of the proof techniques we've seen—Floyd, Levin-Gries and AFR—don't apply. The essential properties here are less about the final state and more about what was sent on the \(\mathit{Out}\) channel.

Therefore, the only proof technique that would be of use here is the compositional method.

The last part of this question is one I probably wouldn't ask, since we haven't covered cryptographic protocols (and how to verify them) at all.

You know the answer to (a) from the lectures.

You can solve this with pen-and-paper reasoning or, since it's a take-home exam, you could ask Spin.

Signal-and-continue means \(E = W < S\). This makes achieving FIFO withdrawal order rather subtle.

Ah, Lamport clocks. No proof method is specified, nor is one applicable since the algorithm is specified in prose. Go for a prose proof.

A1 is ambiguously worded. Are we waiting for any old message with a greater timestamp, or specifically for REPLY messages? Does it matter?

You can ignore this question, since we didn't cover x86-TSO (a model of weak memory concurrency on x86 hardware).

You're allowed to have a process for the crate. The question was reskinned with this clarification, and an animal theme, in the 2017 exam.

DAJ would be great for this kind of thing, except it doesn't support the required number of generals or rounds for either subquestion.

The \(\rightarrow\) on the transition labels is the separator between condition and update function. This year, we write it as a semicolon.

The question is about C, but you can approach the question ignoring any C-specific details—just pretend it's the usual pseudocode. As an aside, note that the volatile keyword in C has different semantics than volatile in Java.

The question doesn't specify what kind of semaphore \(s\) is. Your transition diagrams may be different depending on whether you consider \(s\) to be a busy-wait, weak or strong semaphore.

The question doesn't specify the precedence of the processes. Assume either \(E < S < W\) or \(E = W < S\). Or better yet, try both. Beware that a correct monitor in one precedence specification may be incorrect in another.

Think about whether your channels are synchronous or asynchronous.

The \(\rightarrow\) on the transition labels is the separator between condition and update function. This year, we write it as $;$.

You'll have to assume FIFO channels here.

This notion of duality is inspired by session types, a kind of type system for message-passing programs. They can guarantee that all programs that typecheck are deadlock free.

There were two assumptions I made in my head that I forgot to state in the text of the question:

1. If there are infinitely many locations, you can have acyclic transition diagrams that nonetheless don't converge.
2. A transition diagram that doesn't have a path from the start state to the end state deadlocks even if it's acyclic and has finitely many locations.

In most cases I awarded full marks for otherwise correct answers that rely on some combination of these assumptions.

The ideas from Time, Clocks and the Ordering of Events in a Distributed System can seem rather obvious in hindsight. This question helps illustrate why the paper was written in the first place: as a response to people getting their algorithms wrong because they didn't have the thinking tools on offer in the paper. Once you have them, it's relatively easy to see, and fix, the problem with Johnson and Thomas' algorithm; questions (b)-(d) invite you to do just that.